<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>ProofAsst</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="ProofAsst";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/pa/PreprocessRequest.html" title="class in mmj.pa"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/pa/ProofAsstCursor.html" title="class in mmj.pa"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/pa/ProofAsst.html" target="_top">Frames</a></li>
<li><a href="ProofAsst.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.pa</div>
<h2 title="Class ProofAsst" class="title">Class ProofAsst</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li>mmj.pa.ProofAsst</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<dl>
<dt>All Implemented Interfaces:</dt>
<dd><a href="../../mmj/tl/TheoremLoaderCommitListener.html" title="interface in mmj.tl">TheoremLoaderCommitListener</a></dd>
</dl>
<hr>
<br>
<pre>public class <span class="strong">ProofAsst</span>
extends java.lang.Object
implements <a href="../../mmj/tl/TheoremLoaderCommitListener.html" title="interface in mmj.tl">TheoremLoaderCommitListener</a></pre>
<div class="block">The <code>ProofAsst</code>, along with the rest of the <code>mmj.pa</code> package
 provides a graphical user interface (GUI) facility for developing Metamath
 proofs. <code>ProofAsst</code> is the go-to guy, essentially a control module that
 knows where to go to get things done. It is invoked by
 mmj.util.ProofAsstBoss.java, and invokes mmj.pa.ProofAsstGUI, among others.
 Nomenclature: a proof-in-progress is implemented by the
 mmj.pa.ProofWorksheet.java class. A large quantity of information and useful
 stuff is contained in mmj.pa.PaConstants.java.</div>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/pa/ProofAsst.html#ProofAsst(mmj.pa.ProofAsstPreferences, mmj.lang.LogicalSystem, mmj.verify.Grammar, mmj.verify.VerifyProofs, mmj.tl.TheoremLoader)">ProofAsst</a></strong>(<a href="../../mmj/pa/ProofAsstPreferences.html" title="class in mmj.pa">ProofAsstPreferences</a>&nbsp;proofAsstPreferences,
         <a href="../../mmj/lang/LogicalSystem.html" title="class in mmj.lang">LogicalSystem</a>&nbsp;logicalSystem,
         <a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
         <a href="../../mmj/verify/VerifyProofs.html" title="class in mmj.verify">VerifyProofs</a>&nbsp;verifyProofs,
         <a href="../../mmj/tl/TheoremLoader.html" title="class in mmj.tl">TheoremLoader</a>&nbsp;theoremLoader)</code>
<div class="block">Constructor.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#commit(mmj.tl.MMTTheoremSet)">commit</a></strong>(<a href="../../mmj/tl/MMTTheoremSet.html" title="class in mmj.tl">MMTTheoremSet</a>&nbsp;mmtTheoremSet)</code>
<div class="block">Applies a set of updates from the TheoremLoader as specified in the
 mmtTheoremSet object to the ProofAsst local caches of data.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#doGUI(mmj.lang.Messages)">doGUI</a></strong>(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;m)</code>
<div class="block">Triggers the Proof Assistant GUI.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#exportOneTheorem(java.lang.String)">exportOneTheorem</a></strong>(java.lang.String&nbsp;theoremLabel)</code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#exportOneTheorem(mmj.lang.Theorem)">exportOneTheorem</a></strong>(<a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;theorem)</code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#exportToFile(java.io.Writer, mmj.lang.Messages, java.lang.Boolean, java.lang.Integer, mmj.lang.Theorem, mmj.util.OutputBoss)">exportToFile</a></strong>(java.io.Writer&nbsp;exportWriter,
            <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
            java.lang.Boolean&nbsp;selectorAll,
            java.lang.Integer&nbsp;selectorCount,
            <a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;selectorTheorem,
            <a href="../../mmj/util/OutputBoss.html" title="class in mmj.util">OutputBoss</a>&nbsp;outputBoss)</code>
<div class="block">Export Theorem proofs to a given Writer.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#exportViaGMFF(java.lang.String)">exportViaGMFF</a></strong>(java.lang.String&nbsp;proofText)</code>
<div class="block">Invokes GMFF to export the current Proof Worksheet.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#extractTheoremToMMTFolder(mmj.lang.Theorem)">extractTheoremToMMTFolder</a></strong>(<a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;theorem)</code>
<div class="block">Invokes TheoremLoader to extract a theorem to the MMT Folder.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#getExistingProof(mmj.lang.Theorem, boolean, boolean)">getExistingProof</a></strong>(<a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;oldTheorem,
                boolean&nbsp;exportFormatUnified,
                boolean&nbsp;hypsRandomized)</code>
<div class="block">Builds ProofWorksheet for an existing theorem.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#getInitializedOK()">getInitializedOK</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/LogicalSystem.html" title="class in mmj.lang">LogicalSystem</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#getLogicalSystem()">getLogicalSystem</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#getMessages()">getMessages</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#getNextProof(int, boolean, boolean)">getNextProof</a></strong>(int&nbsp;currProofMaxSeq,
            boolean&nbsp;exportFormatUnified,
            boolean&nbsp;hypsRandomized)</code>
<div class="block">Builds ProofWorksheet for the next theorem after a given MObj sequence
 number.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#getPreviousProof(int, boolean, boolean)">getPreviousProof</a></strong>(int&nbsp;currProofMaxSeq,
                boolean&nbsp;exportFormatUnified,
                boolean&nbsp;hypsRandomized)</code>
<div class="block">Builds ProofWorksheet for the first theorem before a given MObj sequence
 number.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/pa/ProofAsstGUI.html" title="class in mmj.pa">ProofAsstGUI</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#getProofAsstGUI()">getProofAsstGUI</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>java.util.List&lt;<a href="../../mmj/lang/Assrt.html" title="class in mmj.lang">Assrt</a>&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#getSortedAssrtSearchList()">getSortedAssrtSearchList</a></strong>()</code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>java.lang.Iterable&lt;<a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#getSortedSkipSeqTheoremIterable(java.lang.String)">getSortedSkipSeqTheoremIterable</a></strong>(java.lang.String&nbsp;startTheoremLabel)</code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#getStmt(java.lang.String)">getStmt</a></strong>(java.lang.String&nbsp;s)</code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#getTheorem(java.lang.String)">getTheorem</a></strong>(java.lang.String&nbsp;theoremLabel)</code>
<div class="block">Fetches a Theorem using an input Label String.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#importFromFileAndUnify(java.io.Reader, mmj.lang.Messages, java.lang.Boolean, java.lang.Integer, mmj.lang.Theorem, mmj.util.OutputBoss, boolean)">importFromFileAndUnify</a></strong>(java.io.Reader&nbsp;importReader,
                      <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                      java.lang.Boolean&nbsp;selectorAll,
                      java.lang.Integer&nbsp;selectorCount,
                      <a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;selectorTheorem,
                      <a href="../../mmj/util/OutputBoss.html" title="class in mmj.util">OutputBoss</a>&nbsp;outputBoss,
                      boolean&nbsp;asciiRetest)</code>
<div class="block">Import Theorem proofs from a given Reader.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#importFromMemoryAndUnify(mmj.lang.Messages, java.lang.Boolean, java.lang.Integer, mmj.lang.Theorem, mmj.util.OutputBoss, boolean)">importFromMemoryAndUnify</a></strong>(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                        java.lang.Boolean&nbsp;selectorAll,
                        java.lang.Integer&nbsp;selectorCount,
                        <a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;selectorTheorem,
                        <a href="../../mmj/util/OutputBoss.html" title="class in mmj.util">OutputBoss</a>&nbsp;outputBoss,
                        boolean&nbsp;asciiRetest)</code>
<div class="block">Import Theorem proofs from memory and unifies.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#initializeLookupTables(mmj.lang.Messages)">initializeLookupTables</a></strong>(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)</code>
<div class="block">Initialized Unification lookup tables, etc.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#loadTheoremsFromMMTFolder()">loadTheoremsFromMMTFolder</a></strong>()</code>
<div class="block">Invokes TheoremLoader to load all theorems in the MMT Folder.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#preprocessRequestBatchTest(java.lang.String, mmj.lang.Messages, mmj.util.OutputBoss, mmj.pa.PreprocessRequest)">preprocessRequestBatchTest</a></strong>(java.lang.String&nbsp;proofText,
                          <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                          <a href="../../mmj/util/OutputBoss.html" title="class in mmj.util">OutputBoss</a>&nbsp;outputBoss,
                          <a href="../../mmj/pa/PreprocessRequest.html" title="class in mmj.pa">PreprocessRequest</a>&nbsp;preprocessRequest)</code>
<div class="block">Exercises the PreprocessRequest code for one proof.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>java.util.List&lt;<a href="../../mmj/lang/Assrt.html" title="class in mmj.lang">Assrt</a>&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#sortAssrtListForSearch(java.util.List)">sortAssrtListForSearch</a></strong>(java.util.List&lt;<a href="../../mmj/lang/Assrt.html" title="class in mmj.lang">Assrt</a>&gt;&nbsp;list)</code>&nbsp;</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#startNewNextProof(int)">startNewNextProof</a></strong>(int&nbsp;currProofMaxSeq)</code>
<div class="block">Builds new ProofWorksheet for the next theorem after the current theorem
 sequence number on the ProofAsstGUI.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#startNewProof(java.lang.String)">startNewProof</a></strong>(java.lang.String&nbsp;newTheoremLabel)</code>
<div class="block">Builds new ProofWorksheet for a theorem.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#stepSelectorBatchTest(java.io.Reader, mmj.lang.Messages, mmj.util.OutputBoss, int, int)">stepSelectorBatchTest</a></strong>(java.io.Reader&nbsp;importReader,
                     <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                     <a href="../../mmj/util/OutputBoss.html" title="class in mmj.util">OutputBoss</a>&nbsp;outputBoss,
                     int&nbsp;cursorPos,
                     int&nbsp;selectionNumber)</code>
<div class="block">Exercises the StepSelectorSearch for one proof.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#tmffReformat(boolean, java.lang.String, int)">tmffReformat</a></strong>(boolean&nbsp;inputCursorStep,
            java.lang.String&nbsp;proofText,
            int&nbsp;inputCursorPos)</code>
<div class="block">Reformats a ProofWorksheet using TMFF.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#unify(boolean, boolean, java.lang.String, mmj.pa.PreprocessRequest, mmj.pa.StepRequest, mmj.tl.TLRequest, int)">unify</a></strong>(boolean&nbsp;renumReq,
     boolean&nbsp;noConvertWV,
     java.lang.String&nbsp;proofText,
     <a href="../../mmj/pa/PreprocessRequest.html" title="class in mmj.pa">PreprocessRequest</a>&nbsp;preprocessRequest,
     <a href="../../mmj/pa/StepRequest.html" title="class in mmj.pa">StepRequest</a>&nbsp;stepRequest,
     <a href="../../mmj/tl/TLRequest.html" title="class in mmj.tl">TLRequest</a>&nbsp;tlRequest,
     int&nbsp;inputCursorPos)</code>
<div class="block">Attempts Unification for a proof contained in a String proof text area.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/pa/ProofAsst.html#verifyAllProofs()">verifyAllProofs</a></strong>()</code>
<div class="block">Verifies all proofs in the Logical System</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="ProofAsst(mmj.pa.ProofAsstPreferences, mmj.lang.LogicalSystem, mmj.verify.Grammar, mmj.verify.VerifyProofs, mmj.tl.TheoremLoader)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>ProofAsst</h4>
<pre>public&nbsp;ProofAsst(<a href="../../mmj/pa/ProofAsstPreferences.html" title="class in mmj.pa">ProofAsstPreferences</a>&nbsp;proofAsstPreferences,
         <a href="../../mmj/lang/LogicalSystem.html" title="class in mmj.lang">LogicalSystem</a>&nbsp;logicalSystem,
         <a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
         <a href="../../mmj/verify/VerifyProofs.html" title="class in mmj.verify">VerifyProofs</a>&nbsp;verifyProofs,
         <a href="../../mmj/tl/TheoremLoader.html" title="class in mmj.tl">TheoremLoader</a>&nbsp;theoremLoader)</pre>
<div class="block">Constructor.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>proofAsstPreferences</code> - variable settings</dd><dd><code>logicalSystem</code> - the loaded Metamath data</dd><dd><code>grammar</code> - the mmj.verify.Grammar object</dd><dd><code>verifyProofs</code> - the mmj.verify.VerifyProofs object</dd><dd><code>theoremLoader</code> - the mmj.tl.TheoremLoader object</dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="doGUI(mmj.lang.Messages)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>doGUI</h4>
<pre>public&nbsp;void&nbsp;doGUI(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;m)</pre>
<div class="block">Triggers the Proof Assistant GUI.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>m</code> - the mmj.lang.Messages object used to store error and
            informational messages.</dd></dl>
</li>
</ul>
<a name="getInitializedOK()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getInitializedOK</h4>
<pre>public&nbsp;boolean&nbsp;getInitializedOK()</pre>
<dl><dt><span class="strong">Returns:</span></dt><dd>initializedOK flag.</dd></dl>
</li>
</ul>
<a name="getLogicalSystem()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getLogicalSystem</h4>
<pre>public&nbsp;<a href="../../mmj/lang/LogicalSystem.html" title="class in mmj.lang">LogicalSystem</a>&nbsp;getLogicalSystem()</pre>
</li>
</ul>
<a name="getMessages()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getMessages</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;getMessages()</pre>
</li>
</ul>
<a name="getProofAsstGUI()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getProofAsstGUI</h4>
<pre>public&nbsp;<a href="../../mmj/pa/ProofAsstGUI.html" title="class in mmj.pa">ProofAsstGUI</a>&nbsp;getProofAsstGUI()</pre>
</li>
</ul>
<a name="sortAssrtListForSearch(java.util.List)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>sortAssrtListForSearch</h4>
<pre>public&nbsp;java.util.List&lt;<a href="../../mmj/lang/Assrt.html" title="class in mmj.lang">Assrt</a>&gt;&nbsp;sortAssrtListForSearch(java.util.List&lt;<a href="../../mmj/lang/Assrt.html" title="class in mmj.lang">Assrt</a>&gt;&nbsp;list)</pre>
</li>
</ul>
<a name="initializeLookupTables(mmj.lang.Messages)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>initializeLookupTables</h4>
<pre>public&nbsp;boolean&nbsp;initializeLookupTables(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages)</pre>
<div class="block">Initialized Unification lookup tables, etc. for Unification.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>messages</code> - the mmj.lang.Messages object used to store error and
            informational messages.</dd>
<dt><span class="strong">Returns:</span></dt><dd>initializedOK flag.</dd></dl>
</li>
</ul>
<a name="getSortedAssrtSearchList()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getSortedAssrtSearchList</h4>
<pre>public&nbsp;java.util.List&lt;<a href="../../mmj/lang/Assrt.html" title="class in mmj.lang">Assrt</a>&gt;&nbsp;getSortedAssrtSearchList()</pre>
</li>
</ul>
<a name="commit(mmj.tl.MMTTheoremSet)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>commit</h4>
<pre>public&nbsp;void&nbsp;commit(<a href="../../mmj/tl/MMTTheoremSet.html" title="class in mmj.tl">MMTTheoremSet</a>&nbsp;mmtTheoremSet)</pre>
<div class="block">Applies a set of updates from the TheoremLoader as specified in the
 mmtTheoremSet object to the ProofAsst local caches of data.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/tl/TheoremLoaderCommitListener.html#commit(mmj.tl.MMTTheoremSet)">commit</a></code>&nbsp;in interface&nbsp;<code><a href="../../mmj/tl/TheoremLoaderCommitListener.html" title="interface in mmj.tl">TheoremLoaderCommitListener</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>mmtTheoremSet</code> - MMTTheoremSet object containing the adds and updates
            already made to theorems in the LogicalSystem.</dd></dl>
</li>
</ul>
<a name="verifyAllProofs()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>verifyAllProofs</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;verifyAllProofs()</pre>
<div class="block">Verifies all proofs in the Logical System
 <p>
 This is here because the Proof Assistant GUI doesn't know how to do
 anything...</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>Messages object.</dd></dl>
</li>
</ul>
<a name="loadTheoremsFromMMTFolder()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>loadTheoremsFromMMTFolder</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;loadTheoremsFromMMTFolder()</pre>
<div class="block">Invokes TheoremLoader to load all theorems in the MMT Folder.
 <p>
 This is here because the Proof Assistant GUI doesn't know how to do
 anything...</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>Messages object.</dd></dl>
</li>
</ul>
<a name="exportViaGMFF(java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>exportViaGMFF</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;exportViaGMFF(java.lang.String&nbsp;proofText)</pre>
<div class="block">Invokes GMFF to export the current Proof Worksheet.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>proofText</code> - Proof Worksheet text string.</dd>
<dt><span class="strong">Returns:</span></dt><dd>Messages object.</dd></dl>
</li>
</ul>
<a name="extractTheoremToMMTFolder(mmj.lang.Theorem)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>extractTheoremToMMTFolder</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;extractTheoremToMMTFolder(<a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;theorem)</pre>
<div class="block">Invokes TheoremLoader to extract a theorem to the MMT Folder.
 <p>
 This is here because the Proof Assistant GUI doesn't know how to do
 anything...</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>theorem</code> - the theorem to extract</dd>
<dt><span class="strong">Returns:</span></dt><dd>Messages object.</dd></dl>
</li>
</ul>
<a name="startNewProof(java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>startNewProof</h4>
<pre>public&nbsp;<a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a>&nbsp;startNewProof(java.lang.String&nbsp;newTheoremLabel)</pre>
<div class="block">Builds new ProofWorksheet for a theorem.
 <p>
 Note: this method is called by ProofAsstGUI.java!
 <p>
 Note that the output ProofWorksheet is skeletal and is destined for a
 straight-shot, output to the GUI screen. The ProofAsst and its components
 retain no memory of a ProofWorksheet between screen actions. Each time
 the user requests a new action the text is scraped off the screen and
 built into a new ProofWorksheet object!
 <p>
 Notice also that this function just invokes a ProofWorksheet constructor.
 Why? Because the ProofAsstGUI.java program has no access to or knowledge
 of LogicalSystem, Grammar, etc. The only external knowledge it has is
 ProofAsstPreferences.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>newTheoremLabel</code> - the name of the new proof</dd>
<dt><span class="strong">Returns:</span></dt><dd>ProofWorksheet initialized skeleton proof</dd></dl>
</li>
</ul>
<a name="startNewNextProof(int)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>startNewNextProof</h4>
<pre>public&nbsp;<a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a>&nbsp;startNewNextProof(int&nbsp;currProofMaxSeq)</pre>
<div class="block">Builds new ProofWorksheet for the next theorem after the current theorem
 sequence number on the ProofAsstGUI.
 <p>
 Note: this method is called by ProofAsstGUI.java!
 <p>
 This function is provided for students who wish to work their way through
 Metamath databases such as set.mm and prove each theorem. It is like
 Forward-GetProof except that it returns a skeletal Proof Worksheet, and
 thus helps the student by not revealing the contents of the existing
 proof in the Metamath database.
 <p>
 Note that the output ProofWorksheet is skeletal and is destined for a
 straight-shot, output to the GUI screen. The ProofAsst and its components
 retain no memory of a ProofWorksheet between screen actions. Each time
 the user requests a new action the text is scraped off the screen and
 built into a new ProofWorksheet object!
 <p>
 Notice also that this function just invokes a ProofWorksheet constructor.
 Why? Because the ProofAsstGUI.java program has no access to or knowledge
 of LogicalSystem, Grammar, etc. The only external knowledge it has is
 ProofAsstPreferences.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>currProofMaxSeq</code> - sequence number of current proof on ProofAsstGUI
            screen.</dd>
<dt><span class="strong">Returns:</span></dt><dd>ProofWorksheet initialized skeleton proof</dd></dl>
</li>
</ul>
<a name="getTheorem(java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getTheorem</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;getTheorem(java.lang.String&nbsp;theoremLabel)</pre>
<div class="block">Fetches a Theorem using an input Label String.
 <p>
 Note: this method is called by ProofAsstGUI.java!</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>theoremLabel</code> - label of Theorem to retrieve from statement table.</dd>
<dt><span class="strong">Returns:</span></dt><dd>Theorem or null if Label not found or is not a Theorem Stmt
         label.</dd></dl>
</li>
</ul>
<a name="getStmt(java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getStmt</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&nbsp;getStmt(java.lang.String&nbsp;s)</pre>
</li>
</ul>
<a name="getExistingProof(mmj.lang.Theorem, boolean, boolean)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getExistingProof</h4>
<pre>public&nbsp;<a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a>&nbsp;getExistingProof(<a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;oldTheorem,
                              boolean&nbsp;exportFormatUnified,
                              boolean&nbsp;hypsRandomized)</pre>
<div class="block">Builds ProofWorksheet for an existing theorem.
 <p>
 Note: this method is called by ProofAsstGUI.java!</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>oldTheorem</code> - theorem to get</dd><dd><code>exportFormatUnified</code> - true means include step Ref labels</dd><dd><code>hypsRandomized</code> - true means step Hyps randomized on ProofWorksheet.</dd>
<dt><span class="strong">Returns:</span></dt><dd>ProofWorksheet initialized.</dd></dl>
</li>
</ul>
<a name="getNextProof(int, boolean, boolean)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getNextProof</h4>
<pre>public&nbsp;<a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a>&nbsp;getNextProof(int&nbsp;currProofMaxSeq,
                          boolean&nbsp;exportFormatUnified,
                          boolean&nbsp;hypsRandomized)</pre>
<div class="block">Builds ProofWorksheet for the next theorem after a given MObj sequence
 number.
 <p>
 The search wraps to the start if the end is reached.
 <p>
 Note: The search list excludes any Theorems excluded by the user from
 Proof Unification (see RunParm ProofAsstUnifySearchExclude). The
 exclusion is made for technical reasons (expediency) -- if you don't like
 it a whole lot we can change it.
 <p>
 Note: this method is called by ProofAsstGUI.java!</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>currProofMaxSeq</code> - sequence number of ProofWorksheet from
            ProofAsstGUI currProofMaxSeq field.</dd><dd><code>exportFormatUnified</code> - true means include step Ref labels</dd><dd><code>hypsRandomized</code> - true means step Hyps randomized on ProofWorksheet.</dd>
<dt><span class="strong">Returns:</span></dt><dd>ProofWorksheet initialized.</dd></dl>
</li>
</ul>
<a name="getPreviousProof(int, boolean, boolean)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getPreviousProof</h4>
<pre>public&nbsp;<a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a>&nbsp;getPreviousProof(int&nbsp;currProofMaxSeq,
                              boolean&nbsp;exportFormatUnified,
                              boolean&nbsp;hypsRandomized)</pre>
<div class="block">Builds ProofWorksheet for the first theorem before a given MObj sequence
 number.
 <p>
 The search wraps to the end if the start is reached.
 <p>
 Note: The search list excludes any Theorems excluded by the user from
 Proof Unification (see RunParm ProofAsstUnifySearchExclude). The
 exclusion is made for technical reasons (expediency) -- if you don't like
 it a whole lot we can change it.
 <p>
 Note: this method is called by ProofAsstGUI.java!</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>currProofMaxSeq</code> - sequence number of ProofWorksheet from
            ProofAsstGUI currProofMaxSeq field.</dd><dd><code>exportFormatUnified</code> - true means include step Ref labels</dd><dd><code>hypsRandomized</code> - true means step Hyps randomized on ProofWorksheet.</dd>
<dt><span class="strong">Returns:</span></dt><dd>ProofWorksheet initialized.</dd></dl>
</li>
</ul>
<a name="unify(boolean, boolean, java.lang.String, mmj.pa.PreprocessRequest, mmj.pa.StepRequest, mmj.tl.TLRequest, int)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>unify</h4>
<pre>public&nbsp;<a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a>&nbsp;unify(boolean&nbsp;renumReq,
                   boolean&nbsp;noConvertWV,
                   java.lang.String&nbsp;proofText,
                   <a href="../../mmj/pa/PreprocessRequest.html" title="class in mmj.pa">PreprocessRequest</a>&nbsp;preprocessRequest,
                   <a href="../../mmj/pa/StepRequest.html" title="class in mmj.pa">StepRequest</a>&nbsp;stepRequest,
                   <a href="../../mmj/tl/TLRequest.html" title="class in mmj.tl">TLRequest</a>&nbsp;tlRequest,
                   int&nbsp;inputCursorPos)</pre>
<div class="block">Attempts Unification for a proof contained in a String proof text area.
 <p>
 Note: this method is called by ProofAsstGUI.java!
 <p>
 The ProofWorksheetParser class is used to parse the input proof text. The
 reason for using this intermediary is that the system is designed to be
 able to read a file of proof texts (which is a feature designed for
 testing purposes, but still available to a user via the BatchMMJ2
 facility.)</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>proofText</code> - proof text from ProofAsstGUI screen, or any String
            conforming to the formatting rules of ProofAsst.</dd><dd><code>renumReq</code> - renumbering of proof steps requested</dd><dd><code>noConvertWV</code> - true if we should not replace work vars with dummy
            vars in derivation steps</dd><dd><code>preprocessRequest</code> - if not null specifies an editing operation to be
            applied to the proof text before other processing.</dd><dd><code>inputCursorPos</code> - caret offset plus one of input or -1 if caret pos
            unavailable to caller.</dd><dd><code>stepRequest</code> - may be null, or StepSelector Search or Choice request
            and will be loaded into the ProofWorksheet.</dd><dd><code>tlRequest</code> - may be null or a TLRequest.</dd>
<dt><span class="strong">Returns:</span></dt><dd>ProofWorksheet unified.</dd></dl>
</li>
</ul>
<a name="tmffReformat(boolean, java.lang.String, int)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>tmffReformat</h4>
<pre>public&nbsp;<a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a>&nbsp;tmffReformat(boolean&nbsp;inputCursorStep,
                          java.lang.String&nbsp;proofText,
                          int&nbsp;inputCursorPos)</pre>
<div class="block">Reformats a ProofWorksheet using TMFF.
 <p>
 Note: this method is called by ProofAsstGUI.java!
 <p>
 Reformatting is not attempted if the ProofWorksheet has structural errors
 (returned from the parser).</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>inputCursorStep</code> - set to true to reformat just the proof step
            underneath the cursor.</dd><dd><code>proofText</code> - proof text from ProofAsstGUI screen, or any String
            conforming to the formatting rules of ProofAsst.</dd><dd><code>inputCursorPos</code> - caret offset plus one of input or -1 if caret pos
            unavailable to caller.</dd>
<dt><span class="strong">Returns:</span></dt><dd>ProofWorksheet reformatted, or not, if errors.</dd></dl>
</li>
</ul>
<a name="importFromMemoryAndUnify(mmj.lang.Messages, java.lang.Boolean, java.lang.Integer, mmj.lang.Theorem, mmj.util.OutputBoss, boolean)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>importFromMemoryAndUnify</h4>
<pre>public&nbsp;void&nbsp;importFromMemoryAndUnify(<a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                            java.lang.Boolean&nbsp;selectorAll,
                            java.lang.Integer&nbsp;selectorCount,
                            <a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;selectorTheorem,
                            <a href="../../mmj/util/OutputBoss.html" title="class in mmj.util">OutputBoss</a>&nbsp;outputBoss,
                            boolean&nbsp;asciiRetest)</pre>
<div class="block">Import Theorem proofs from memory and unifies.
 <p>
 This is a simulation routine for testing purposes.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>messages</code> - Messages object for output messages.</dd><dd><code>selectorAll</code> - true if process all theorems, false or null, ignore
            param.</dd><dd><code>selectorCount</code> - use if not null to restrict the number of theorems
            present.</dd><dd><code>selectorTheorem</code> - just process one theorem, ignore selectorCount and
            selectorAll.</dd><dd><code>outputBoss</code> - mmj.util.OutputBoss object, if not null means, please
            print the proof test.</dd><dd><code>asciiRetest</code> - instructs program to re-unify the output Proof
            Worksheet text after unification.</dd></dl>
</li>
</ul>
<a name="importFromFileAndUnify(java.io.Reader, mmj.lang.Messages, java.lang.Boolean, java.lang.Integer, mmj.lang.Theorem, mmj.util.OutputBoss, boolean)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>importFromFileAndUnify</h4>
<pre>public&nbsp;void&nbsp;importFromFileAndUnify(java.io.Reader&nbsp;importReader,
                          <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                          java.lang.Boolean&nbsp;selectorAll,
                          java.lang.Integer&nbsp;selectorCount,
                          <a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;selectorTheorem,
                          <a href="../../mmj/util/OutputBoss.html" title="class in mmj.util">OutputBoss</a>&nbsp;outputBoss,
                          boolean&nbsp;asciiRetest)</pre>
<div class="block">Import Theorem proofs from a given Reader.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>importReader</code> - source of proofs</dd><dd><code>messages</code> - Messages object for output messages.</dd><dd><code>selectorAll</code> - true if process all theorems, false or null, ignore
            param.</dd><dd><code>selectorCount</code> - use if not null to restrict the number of theorems
            present.</dd><dd><code>selectorTheorem</code> - just process one theorem, ignore selectorCount and
            selectorAll.</dd><dd><code>outputBoss</code> - mmj.util.OutputBoss object, if not null means, please
            print the proof test.</dd><dd><code>asciiRetest</code> - instructs program to re-unify the output Proof
            Worksheet text after unification.</dd></dl>
</li>
</ul>
<a name="preprocessRequestBatchTest(java.lang.String, mmj.lang.Messages, mmj.util.OutputBoss, mmj.pa.PreprocessRequest)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>preprocessRequestBatchTest</h4>
<pre>public&nbsp;void&nbsp;preprocessRequestBatchTest(java.lang.String&nbsp;proofText,
                              <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                              <a href="../../mmj/util/OutputBoss.html" title="class in mmj.util">OutputBoss</a>&nbsp;outputBoss,
                              <a href="../../mmj/pa/PreprocessRequest.html" title="class in mmj.pa">PreprocessRequest</a>&nbsp;preprocessRequest)</pre>
<div class="block">Exercises the PreprocessRequest code for one proof.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>proofText</code> - one Proof Text Area in a String.</dd><dd><code>messages</code> - Messages object for output messages.</dd><dd><code>outputBoss</code> - mmj.util.OutputBoss object, if not null means, please
            print the proof test.</dd><dd><code>preprocessRequest</code> - to apply before unification</dd></dl>
</li>
</ul>
<a name="stepSelectorBatchTest(java.io.Reader, mmj.lang.Messages, mmj.util.OutputBoss, int, int)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>stepSelectorBatchTest</h4>
<pre>public&nbsp;void&nbsp;stepSelectorBatchTest(java.io.Reader&nbsp;importReader,
                         <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                         <a href="../../mmj/util/OutputBoss.html" title="class in mmj.util">OutputBoss</a>&nbsp;outputBoss,
                         int&nbsp;cursorPos,
                         int&nbsp;selectionNumber)</pre>
<div class="block">Exercises the StepSelectorSearch for one proof.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>importReader</code> - source of proofs</dd><dd><code>messages</code> - Messages object for output messages.</dd><dd><code>outputBoss</code> - mmj.util.OutputBoss object, if not null means, please
            print the proof test.</dd><dd><code>cursorPos</code> - offset of input cursor.</dd><dd><code>selectionNumber</code> - choice from StepSelectorResults</dd></dl>
</li>
</ul>
<a name="exportToFile(java.io.Writer, mmj.lang.Messages, java.lang.Boolean, java.lang.Integer, mmj.lang.Theorem, mmj.util.OutputBoss)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>exportToFile</h4>
<pre>public&nbsp;void&nbsp;exportToFile(java.io.Writer&nbsp;exportWriter,
                <a href="../../mmj/lang/Messages.html" title="class in mmj.lang">Messages</a>&nbsp;messages,
                java.lang.Boolean&nbsp;selectorAll,
                java.lang.Integer&nbsp;selectorCount,
                <a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;selectorTheorem,
                <a href="../../mmj/util/OutputBoss.html" title="class in mmj.util">OutputBoss</a>&nbsp;outputBoss)</pre>
<div class="block">Export Theorem proofs to a given Writer.
 <p>
 Uses ProofAsstPreferences.getExportFormatUnified() to determine whether
 output proof derivation steps contain Ref statement labels (if "unified"
 then yes, add labels.)
 <p>
 An incomplete input proof generates an incomplete output proof as well as
 an error message.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>exportWriter</code> - destination for output proofs.</dd><dd><code>messages</code> - Messages object for output messages.</dd><dd><code>selectorAll</code> - true if process all theorems, false or null, ignore
            param.</dd><dd><code>selectorCount</code> - use if not null to restrict the number of theorems
            present.</dd><dd><code>selectorTheorem</code> - just process one theorem, ignore selectorCount and
            selectorAll.</dd><dd><code>outputBoss</code> - mmj.util.OutputBoss object, if not null means, please
            print the proof test.</dd></dl>
</li>
</ul>
<a name="exportOneTheorem(java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>exportOneTheorem</h4>
<pre>public&nbsp;java.lang.String&nbsp;exportOneTheorem(java.lang.String&nbsp;theoremLabel)</pre>
</li>
</ul>
<a name="exportOneTheorem(mmj.lang.Theorem)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>exportOneTheorem</h4>
<pre>public&nbsp;java.lang.String&nbsp;exportOneTheorem(<a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&nbsp;theorem)</pre>
</li>
</ul>
<a name="getSortedSkipSeqTheoremIterable(java.lang.String)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>getSortedSkipSeqTheoremIterable</h4>
<pre>public&nbsp;java.lang.Iterable&lt;<a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a>&gt;&nbsp;getSortedSkipSeqTheoremIterable(java.lang.String&nbsp;startTheoremLabel)
                                                            throws <a href="../../mmj/pa/ProofAsstException.html" title="class in mmj.pa">ProofAsstException</a></pre>
<dl><dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/pa/ProofAsstException.html" title="class in mmj.pa">ProofAsstException</a></code></dd></dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/pa/PreprocessRequest.html" title="class in mmj.pa"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/pa/ProofAsstCursor.html" title="class in mmj.pa"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/pa/ProofAsst.html" target="_top">Frames</a></li>
<li><a href="ProofAsst.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
